es:ES, e, e':E.
(isrcv(e))
 (e':E. (isrcv(e'))  (kind(e') = kind(e)  Knd)  (sender(e') = sender(e)  E)  (e' = e))
 (isrcv(e'))
 (kind(e') = kind(e)  Knd)
 sender(e) loc sender(e') 
 e loc e'  

latex

Definitions

x:A. B(x), (e <loc e'), t  T, {T}, P  Q, s = t, , E, left + right, e loc e' , f(a), EState(T), Id, , x:AB(x), pred!(e;e'), SWellFounded(R(x;y)), loc(e), <a, b>, b, A, P  Q, constant_function(f;A;B), Type, kindcase(k; a.f(a); l,t.g(l;t) ), Knd, x:A  B(x), P & Q, Top, , e < e', r  s, val-axiom(E;V;M;info;pred?;init;Trans;Choose;Send;val;time), , Unit, Msg(M), type List, IdLnk, EOrderAxioms(E; pred?; info), EqDecider(T), ES, let x,y = A in B(x;y), t.1, if b then t else f fi , kind(e), (e < e'), P  Q, P  Q, case b of inl(x) => s(x) | inr(y) => t(y), sender(e), x. t(x), lnk(e), True, T, lnk(k), a < b, sends(l;e), (Msg on l), ||as||, #$n, {i..j}, {x:A| B(x)} , index(e)

Lemmas

es-index wf, int seg wf, length wf1, es-Msgl wf, es-sends wf, es-lnk wf, lnk wf, es-axioms, all functionality wrt iff, implies functionality wrt iff, es-sender wf, assert-eq-knd, es-causle-le, Knd wf, es-kind wf, val-axiom wf, constant function wf, es-locl wf